

LEMMA

External connection implies connection.
=============================
Step 1

? (all x (all y ((ec x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (ec c515802 c515801)) v (c c515802 c515801))


> hypdisj
=============================
Step 3

? (c c515802 c515801)

1. (ec c515802 c515801)

> ((c X Y) <-- (ec X Y))
=============================
Step 4

? (ec c515802 c515801)

1. (~ (c c515802 c515801))
2. (ec c515802 c515801)

> hyp


LEMMA

Proper part implies parthood.
=============================
Step 1

? (all x (all y ((pp x y) => (p x y))))


> revsk
=============================
Step 2

? ((~ (pp c520931 c520930)) v (p c520931 c520930))


> hypdisj
=============================
Step 3

? (p c520931 c520930)

1. (pp c520931 c520930)

> ((p X Y) <-- (pp X Y))
=============================
Step 4

? (pp c520931 c520930)

1. (~ (p c520931 c520930))
2. (pp c520931 c520930)

> hyp


LEMMA

Tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((tpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (tpp c526116 c526115)) v (pp c526116 c526115))


> hypdisj
=============================
Step 3

? (pp c526116 c526115)

1. (tpp c526116 c526115)

> ((pp X Y) <-- (tpp X Y))
=============================
Step 4

? (tpp c526116 c526115)

1. (~ (pp c526116 c526115))
2. (tpp c526116 c526115)

> hyp


LEMMA

Non-tangential proper part implies proper part.
=============================
Step 1

? (all x (all y ((ntpp x y) => (pp x y))))


> revsk
=============================
Step 2

? ((~ (ntpp c531357 c531356)) v (pp c531357 c531356))


> hypdisj
=============================
Step 3

? (pp c531357 c531356)

1. (ntpp c531357 c531356)

> ((pp X Y) <-- (ntpp X Y))
=============================
Step 4

? (ntpp c531357 c531356)

1. (~ (pp c531357 c531356))
2. (ntpp c531357 c531356)

> hyp


LEMMA

Parthood lifts connection from part to whole.
=============================
Step 1

? (all x (all y (all z (((p x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (p c536656 c536655)) v (~ (c c536654 c536656))) v (c c536654 c536655))


> hypdisj
=============================
Step 3

? (c c536654 c536655)

1. (c c536654 c536656)
2. (p c536656 c536655)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var24 c536655)
|
|1. (~ (c c536654 c536655))
|2. (c c536654 c536656)
|3. (p c536656 c536655)
|
|> hyp
=============================
Step 5

? (c c536654 c536656)

1. (~ (c c536654 c536655))
2. (c c536654 c536656)
3. (p c536656 c536655)

> hyp


LEMMA

If x is disconnected from y and y is a tangential proper part of z, then z is not part of x.
=============================
Step 1

? (all x (all y (all z (((dc x y) & (tpp y z)) => (~ (p z x))))))


> revsk
=============================
Step 2

? (((~ (dc c542111 c542110)) v (~ (tpp c542110 c542109))) v (~ (p c542109 c542111)))


> hypdisj
=============================
Step 3

? (~ (p c542109 c542111))

1. (tpp c542110 c542109)
2. (dc c542111 c542110)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 4
|
|? (c Var37 c542109)
|
|1. (p c542109 c542111)
|2. (tpp c542110 c542109)
|3. (dc c542111 c542110)
|
|> ((c Y X) <-- (p Z X) (c Y Z))
||=============================
||Step 5
||
||? (p Var40 c542109)
||
||1. (~ (c Var37 c542109))
||2. (p c542109 c542111)
||3. (tpp c542110 c542109)
||4. (dc c542111 c542110)
||
||> ((p X Y) <-- (pp X Y))
||=============================
||Step 6
||
||? (pp Var40 c542109)
||
||1. (~ (p Var40 c542109))
||2. (~ (c Var37 c542109))
||3. (p c542109 c542111)
||4. (tpp c542110 c542109)
||5. (dc c542111 c542110)
||
||> ((pp X Y) <-- (tpp X Y))
||=============================
||Step 7
||
||? (tpp Var40 c542109)
||
||1. (~ (pp Var40 c542109))
||2. (~ (p Var40 c542109))
||3. (~ (c Var37 c542109))
||4. (p c542109 c542111)
||5. (tpp c542110 c542109)
||6. (dc c542111 c542110)
||
||> hyp
|=============================
|Step 8
|
|? (c c542110 c542110)
|
|1. (~ (c c542110 c542109))
|2. (p c542109 c542111)
|3. (tpp c542110 c542109)
|4. (dc c542111 c542110)
|
|> ((c X X) <--)
=============================
Step 9

? (~ (c c542110 c542111))

1. (p c542109 c542111)
2. (tpp c542110 c542109)
3. (dc c542111 c542110)

> ((~ (c Y X)) <-- (~ (c X Y)))
=============================
Step 10

? (~ (c c542111 c542110))

1. (c c542110 c542111)
2. (p c542109 c542111)
3. (tpp c542110 c542109)
4. (dc c542111 c542110)

> ((~ (c X Y)) <-- (dc X Y))
=============================
Step 11

? (dc c542111 c542110)

1. (c c542111 c542110)
2. (c c542110 c542111)
3. (p c542109 c542111)
4. (tpp c542110 c542109)
5. (dc c542111 c542110)

> hyp


LEMMA

Case split on whether x is connected to z; if not, then dc x z.
=============================
Step 1

? (all x (all y (all z (((dc x y) & (tpp y z)) => ((dc x z) v (c x z))))))


> revsk
=============================
Step 2

? (((~ (dc c547722 c547721)) v (~ (tpp c547721 c547720))) v ((dc c547722 c547720) v (c c547722 c547720)))


> hypdisj
=============================
Step 3

? (c c547722 c547720)

1. (~ (dc c547722 c547720))
2. (tpp c547721 c547720)
3. (dc c547722 c547721)

> ((c X Y) <-- (~ (dc X Y)))
=============================
Step 4

? (~ (dc c547722 c547720))

1. (~ (c c547722 c547720))
2. (~ (dc c547722 c547720))
3. (tpp c547721 c547720)
4. (dc c547722 c547721)

> hyp


LEMMA

If x is connected to z, split on overlap to get ec x z or o x z.
=============================
Step 1

? (all x (all y (all z ((((dc x y) & (tpp y z)) & (c x z)) => ((ec x z) v (o x z))))))


> revsk
=============================
Step 2

? ((((~ (dc c553599 c553598)) v (~ (tpp c553598 c553597))) v (~ (c c553599 c553597))) v ((ec c553599 c553597) v (o c553599 c553597)))


> hypdisj
=============================
Step 3

? (o c553599 c553597)

1. (~ (ec c553599 c553597))
2. (c c553599 c553597)
3. (tpp c553598 c553597)
4. (dc c553599 c553598)

> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|=============================
|Step 4
|
|? (c c553599 c553597)
|
|1. (~ (o c553599 c553597))
|2. (~ (ec c553599 c553597))
|3. (c c553599 c553597)
|4. (tpp c553598 c553597)
|5. (dc c553599 c553598)
|
|> hyp
=============================
Step 5

? (~ (ec c553599 c553597))

1. (~ (o c553599 c553597))
2. (~ (ec c553599 c553597))
3. (c c553599 c553597)
4. (tpp c553598 c553597)
5. (dc c553599 c553598)

> hyp


LEMMA

If x overlaps z and z is not part of x, then either po x z or pp x z.
=============================
Step 1

? (all x (all y (all z (((((dc x y) & (tpp y z)) & (c x z)) & (o x z)) => ((po x z) v (pp x z))))))


> revsk
=============================
Step 2

? (((((~ (dc c559892 c559891)) v (~ (tpp c559891 c559890))) v (~ (c c559892 c559890))) v (~ (o c559892 c559890))) v ((po c559892 c559890) v (pp c559892 c559890)))


> hypdisj
=============================
Step 3

? (pp c559892 c559890)

1. (~ (po c559892 c559890))
2. (o c559892 c559890)
3. (c c559892 c559890)
4. (tpp c559891 c559890)
5. (dc c559892 c559891)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 4
|
|? (p c559892 c559890)
|
|1. (~ (pp c559892 c559890))
|2. (~ (po c559892 c559890))
|3. (o c559892 c559890)
|4. (c c559892 c559890)
|5. (tpp c559891 c559890)
|6. (dc c559892 c559891)
|
|> ((p Y X) <-- (p X Y) (~ (pp X Y)))
||=============================
||Step 5
||
||? (p c559890 c559892)
||
||1. (~ (p c559892 c559890))
||2. (~ (pp c559892 c559890))
||3. (~ (po c559892 c559890))
||4. (o c559892 c559890)
||5. (c c559892 c559890)
||6. (tpp c559891 c559890)
||7. (dc c559892 c559891)
||
||> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
||||=============================
||||Step 6
||||
||||? (o c559892 c559890)
||||
||||1. (~ (p c559890 c559892))
||||2. (~ (p c559892 c559890))
||||3. (~ (pp c559892 c559890))
||||4. (~ (po c559892 c559890))
||||5. (o c559892 c559890)
||||6. (c c559892 c559890)
||||7. (tpp c559891 c559890)
||||8. (dc c559892 c559891)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (~ (p c559892 c559890))
|||
|||1. (~ (p c559890 c559892))
|||2. (~ (p c559892 c559890))
|||3. (~ (pp c559892 c559890))
|||4. (~ (po c559892 c559890))
|||5. (o c559892 c559890)
|||6. (c c559892 c559890)
|||7. (tpp c559891 c559890)
|||8. (dc c559892 c559891)
|||
|||> hyp
||=============================
||Step 8
||
||? (~ (po c559892 c559890))
||
||1. (~ (p c559890 c559892))
||2. (~ (p c559892 c559890))
||3. (~ (pp c559892 c559890))
||4. (~ (po c559892 c559890))
||5. (o c559892 c559890)
||6. (c c559892 c559890)
||7. (tpp c559891 c559890)
||8. (dc c559892 c559891)
||
||> hyp
|=============================
|Step 9
|
|? (~ (pp c559890 c559892))
|
|1. (~ (p c559892 c559890))
|2. (~ (pp c559892 c559890))
|3. (~ (po c559892 c559890))
|4. (o c559892 c559890)
|5. (c c559892 c559890)
|6. (tpp c559891 c559890)
|7. (dc c559892 c559891)
|
|> ((~ (pp X Y)) <-- (~ (p X Y)))
|=============================
|Step 10
|
|? (~ (p c559890 c559892))
|
|1. (pp c559890 c559892)
|2. (~ (p c559892 c559890))
|3. (~ (pp c559892 c559890))
|4. (~ (po c559892 c559890))
|5. (o c559892 c559890)
|6. (c c559892 c559890)
|7. (tpp c559891 c559890)
|8. (dc c559892 c559891)
|
|> ((~ (p Z X)) <-- (dc X Y) (tpp Y Z))
||=============================
||Step 11
||
||? (dc c559892 Var51)
||
||1. (p c559890 c559892)
||2. (pp c559890 c559892)
||3. (~ (p c559892 c559890))
||4. (~ (pp c559892 c559890))
||5. (~ (po c559892 c559890))
||6. (o c559892 c559890)
||7. (c c559892 c559890)
||8. (tpp c559891 c559890)
||9. (dc c559892 c559891)
||
||> hyp
|=============================
|Step 12
|
|? (tpp c559891 c559890)
|
|1. (p c559890 c559892)
|2. (pp c559890 c559892)
|3. (~ (p c559892 c559890))
|4. (~ (pp c559892 c559890))
|5. (~ (po c559892 c559890))
|6. (o c559892 c559890)
|7. (c c559892 c559890)
|8. (tpp c559891 c559890)
|9. (dc c559892 c559891)
|
|> hyp
=============================
Step 13

? (~ (p c559890 c559892))

1. (~ (pp c559892 c559890))
2. (~ (po c559892 c559890))
3. (o c559892 c559890)
4. (c c559892 c559890)
5. (tpp c559891 c559890)
6. (dc c559892 c559891)

> ((~ (p Z X)) <-- (dc X Y) (tpp Y Z))
|=============================
|Step 14
|
|? (dc c559892 Var56)
|
|1. (p c559890 c559892)
|2. (~ (pp c559892 c559890))
|3. (~ (po c559892 c559890))
|4. (o c559892 c559890)
|5. (c c559892 c559890)
|6. (tpp c559891 c559890)
|7. (dc c559892 c559891)
|
|> hyp
=============================
Step 15

? (tpp c559891 c559890)

1. (p c559890 c559892)
2. (~ (pp c559892 c559890))
3. (~ (po c559892 c559890))
4. (o c559892 c559890)
5. (c c559892 c559890)
6. (tpp c559891 c559890)
7. (dc c559892 c559891)

> hyp


LEMMA

Proper part decomposes into tangential or non-tangential proper part.
=============================
Step 1

? (all x (all y ((pp x y) => ((tpp x y) v (ntpp x y)))))


> revsk
=============================
Step 2

? ((~ (pp c566795 c566794)) v ((tpp c566795 c566794) v (ntpp c566795 c566794)))


> hypdisj
=============================
Step 3

? (ntpp c566795 c566794)

1. (~ (tpp c566795 c566794))
2. (pp c566795 c566794)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f560009 Z X Y) Z)))
|=============================
|Step 4
|
|? (pp c566795 c566794)
|
|1. (~ (ntpp c566795 c566794))
|2. (~ (tpp c566795 c566794))
|3. (pp c566795 c566794)
|
|> hyp
=============================
Step 5

? (~ (ec (f560009 c566795 c566794 Var32) c566795))

1. (~ (ntpp c566795 c566794))
2. (~ (tpp c566795 c566794))
3. (pp c566795 c566794)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 6
||
||? (pp c566795 Var36)
||
||1. (ec (f560009 c566795 c566794 Var32) c566795)
||2. (~ (ntpp c566795 c566794))
||3. (~ (tpp c566795 c566794))
||4. (pp c566795 c566794)
||
||> hyp
|=============================
|Step 7
|
|? (ec (f560009 c566795 c566794 Var32) c566794)
|
|1. (ec (f560009 c566795 c566794 Var32) c566795)
|2. (~ (ntpp c566795 c566794))
|3. (~ (tpp c566795 c566794))
|4. (pp c566795 c566794)
|
|> ((ec (f560009 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 8
||
||? (~ (ntpp c566795 c566794))
||
||1. (~ (ec (f560009 c566795 c566794 Var32) c566794))
||2. (ec (f560009 c566795 c566794 Var32) c566795)
||3. (~ (ntpp c566795 c566794))
||4. (~ (tpp c566795 c566794))
||5. (pp c566795 c566794)
||
||> hyp
|=============================
|Step 9
|
|? (pp c566795 c566794)
|
|1. (~ (ec (f560009 c566795 c566794 Var32) c566794))
|2. (ec (f560009 c566795 c566794 Var32) c566795)
|3. (~ (ntpp c566795 c566794))
|4. (~ (tpp c566795 c566794))
|5. (pp c566795 c566794)
|
|> hyp
=============================
Step 10

? (~ (tpp c566795 c566794))

1. (ec (f560009 c566795 c566794 Var32) c566795)
2. (~ (ntpp c566795 c566794))
3. (~ (tpp c566795 c566794))
4. (pp c566795 c566794)

> hyp


LEMMA

Refine the overlap case from po or pp to po or tpp or ntpp.
=============================
Step 1

? (all x (all y (all z (((((dc x y) & (tpp y z)) & (c x z)) & (o x z)) => ((po x z) v ((tpp x z) v (ntpp x z)))))))


> revsk
=============================
Step 2

? (((((~ (dc c573851 c573850)) v (~ (tpp c573850 c573849))) v (~ (c c573851 c573849))) v (~ (o c573851 c573849))) v ((po c573851 c573849) v ((tpp c573851 c573849) v (ntpp c573851 c573849))))


> hypdisj
=============================
Step 3

? (ntpp c573851 c573849)

1. (~ (tpp c573851 c573849))
2. (~ (po c573851 c573849))
3. (o c573851 c573849)
4. (c c573851 c573849)
5. (tpp c573850 c573849)
6. (dc c573851 c573850)

> ((ntpp X Y) <-- (pp X Y) (~ (tpp X Y)))
|=============================
|Step 4
|
|? (pp c573851 c573849)
|
|1. (~ (ntpp c573851 c573849))
|2. (~ (tpp c573851 c573849))
|3. (~ (po c573851 c573849))
|4. (o c573851 c573849)
|5. (c c573851 c573849)
|6. (tpp c573850 c573849)
|7. (dc c573851 c573850)
|
|> ((pp Y Z) <-- (dc Y X) (tpp X Z) (c Y Z) (o Y Z) (~ (po Y Z)))
|||||=============================
|||||Step 5
|||||
|||||? (dc c573851 Var32)
|||||
|||||1. (~ (pp c573851 c573849))
|||||2. (~ (ntpp c573851 c573849))
|||||3. (~ (tpp c573851 c573849))
|||||4. (~ (po c573851 c573849))
|||||5. (o c573851 c573849)
|||||6. (c c573851 c573849)
|||||7. (tpp c573850 c573849)
|||||8. (dc c573851 c573850)
|||||
|||||> hyp
||||=============================
||||Step 6
||||
||||? (tpp c573850 c573849)
||||
||||1. (~ (pp c573851 c573849))
||||2. (~ (ntpp c573851 c573849))
||||3. (~ (tpp c573851 c573849))
||||4. (~ (po c573851 c573849))
||||5. (o c573851 c573849)
||||6. (c c573851 c573849)
||||7. (tpp c573850 c573849)
||||8. (dc c573851 c573850)
||||
||||> hyp
|||=============================
|||Step 7
|||
|||? (c c573851 c573849)
|||
|||1. (~ (pp c573851 c573849))
|||2. (~ (ntpp c573851 c573849))
|||3. (~ (tpp c573851 c573849))
|||4. (~ (po c573851 c573849))
|||5. (o c573851 c573849)
|||6. (c c573851 c573849)
|||7. (tpp c573850 c573849)
|||8. (dc c573851 c573850)
|||
|||> hyp
||=============================
||Step 8
||
||? (o c573851 c573849)
||
||1. (~ (pp c573851 c573849))
||2. (~ (ntpp c573851 c573849))
||3. (~ (tpp c573851 c573849))
||4. (~ (po c573851 c573849))
||5. (o c573851 c573849)
||6. (c c573851 c573849)
||7. (tpp c573850 c573849)
||8. (dc c573851 c573850)
||
||> hyp
|=============================
|Step 9
|
|? (~ (po c573851 c573849))
|
|1. (~ (pp c573851 c573849))
|2. (~ (ntpp c573851 c573849))
|3. (~ (tpp c573851 c573849))
|4. (~ (po c573851 c573849))
|5. (o c573851 c573849)
|6. (c c573851 c573849)
|7. (tpp c573850 c573849)
|8. (dc c573851 c573850)
|
|> hyp
=============================
Step 10

? (~ (tpp c573851 c573849))

1. (~ (ntpp c573851 c573849))
2. (~ (tpp c573851 c573849))
3. (~ (po c573851 c573849))
4. (o c573851 c573849)
5. (c c573851 c573849)
6. (tpp c573850 c573849)
7. (dc c573851 c573850)

> hyp


LEMMA

Combine the local case splits: dc or c; if c then ec or o; if o then po or pp; finally split pp into tpp or ntpp.
=============================
Step 1

? (all x (all y (all z (((dc x y) & (tpp y z)) => (((((dc x z) v (ec x z)) v (po x z)) v (tpp x z)) v (ntpp x z))))))


> revsk
=============================
Step 2

? (((~ (dc c581767 c581766)) v (~ (tpp c581766 c581765))) v (((((dc c581767 c581765) v (ec c581767 c581765)) v (po c581767 c581765)) v (tpp c581767 c581765)) v (ntpp c581767 c581765)))


> hypdisj
=============================
Step 3

? (ntpp c581767 c581765)

1. (~ (tpp c581767 c581765))
2. (~ (po c581767 c581765))
3. (~ (ec c581767 c581765))
4. (~ (dc c581767 c581765))
5. (tpp c581766 c581765)
6. (dc c581767 c581766)

> ((ntpp Y Z) <-- (dc Y X) (tpp X Z) (c Y Z) (o Y Z) (~ (po Y Z)) (~ (tpp Y Z)))
|||||=============================
|||||Step 4
|||||
|||||? (dc c581767 Var35)
|||||
|||||1. (~ (ntpp c581767 c581765))
|||||2. (~ (tpp c581767 c581765))
|||||3. (~ (po c581767 c581765))
|||||4. (~ (ec c581767 c581765))
|||||5. (~ (dc c581767 c581765))
|||||6. (tpp c581766 c581765)
|||||7. (dc c581767 c581766)
|||||
|||||> hyp
||||=============================
||||Step 5
||||
||||? (tpp c581766 c581765)
||||
||||1. (~ (ntpp c581767 c581765))
||||2. (~ (tpp c581767 c581765))
||||3. (~ (po c581767 c581765))
||||4. (~ (ec c581767 c581765))
||||5. (~ (dc c581767 c581765))
||||6. (tpp c581766 c581765)
||||7. (dc c581767 c581766)
||||
||||> hyp
|||=============================
|||Step 6
|||
|||? (c c581767 c581765)
|||
|||1. (~ (ntpp c581767 c581765))
|||2. (~ (tpp c581767 c581765))
|||3. (~ (po c581767 c581765))
|||4. (~ (ec c581767 c581765))
|||5. (~ (dc c581767 c581765))
|||6. (tpp c581766 c581765)
|||7. (dc c581767 c581766)
|||
|||> ((c X Y) <-- (~ (dc X Y)))
|||=============================
|||Step 7
|||
|||? (~ (dc c581767 c581765))
|||
|||1. (~ (c c581767 c581765))
|||2. (~ (ntpp c581767 c581765))
|||3. (~ (tpp c581767 c581765))
|||4. (~ (po c581767 c581765))
|||5. (~ (ec c581767 c581765))
|||6. (~ (dc c581767 c581765))
|||7. (tpp c581766 c581765)
|||8. (dc c581767 c581766)
|||
|||> hyp
||=============================
||Step 8
||
||? (o c581767 c581765)
||
||1. (~ (ntpp c581767 c581765))
||2. (~ (tpp c581767 c581765))
||3. (~ (po c581767 c581765))
||4. (~ (ec c581767 c581765))
||5. (~ (dc c581767 c581765))
||6. (tpp c581766 c581765)
||7. (dc c581767 c581766)
||
||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||=============================
|||Step 9
|||
|||? (c c581767 c581765)
|||
|||1. (~ (o c581767 c581765))
|||2. (~ (ntpp c581767 c581765))
|||3. (~ (tpp c581767 c581765))
|||4. (~ (po c581767 c581765))
|||5. (~ (ec c581767 c581765))
|||6. (~ (dc c581767 c581765))
|||7. (tpp c581766 c581765)
|||8. (dc c581767 c581766)
|||
|||> ((c X Y) <-- (~ (dc X Y)))
|||=============================
|||Step 10
|||
|||? (~ (dc c581767 c581765))
|||
|||1. (~ (c c581767 c581765))
|||2. (~ (o c581767 c581765))
|||3. (~ (ntpp c581767 c581765))
|||4. (~ (tpp c581767 c581765))
|||5. (~ (po c581767 c581765))
|||6. (~ (ec c581767 c581765))
|||7. (~ (dc c581767 c581765))
|||8. (tpp c581766 c581765)
|||9. (dc c581767 c581766)
|||
|||> hyp
||=============================
||Step 11
||
||? (~ (ec c581767 c581765))
||
||1. (~ (o c581767 c581765))
||2. (~ (ntpp c581767 c581765))
||3. (~ (tpp c581767 c581765))
||4. (~ (po c581767 c581765))
||5. (~ (ec c581767 c581765))
||6. (~ (dc c581767 c581765))
||7. (tpp c581766 c581765)
||8. (dc c581767 c581766)
||
||> hyp
|=============================
|Step 12
|
|? (~ (po c581767 c581765))
|
|1. (~ (ntpp c581767 c581765))
|2. (~ (tpp c581767 c581765))
|3. (~ (po c581767 c581765))
|4. (~ (ec c581767 c581765))
|5. (~ (dc c581767 c581765))
|6. (tpp c581766 c581765)
|7. (dc c581767 c581766)
|
|> hyp
=============================
Step 13

? (~ (tpp c581767 c581765))

1. (~ (ntpp c581767 c581765))
2. (~ (tpp c581767 c581765))
3. (~ (po c581767 c581765))
4. (~ (ec c581767 c581765))
5. (~ (dc c581767 c581765))
6. (tpp c581766 c581765)
7. (dc c581767 c581766)

> hyp
